| Definitions | t  T, x:A B(x), a:A fp B(a), 1of(t), Knd, type List, Type,   x. t(x),  x:A. B(x), lnk-decl(l;dt), x:A B(x), P   Q, s = t, False, True, {T}, P  Q, Void, rcv(l,tg), false, KindDeq, eqof(d), f(a), p q,  b, x.A(x), filter(P;l), deq-member(eq;x;L),  b, left+right, , Id, Prop, A,  , a = b, P & Q, P  Q, Unit, source(l), mk-ma, x : v, x dom(f), , only members of L read x, es realizer ind Rrframe compseq tag def, Rsends?(x1), Reffect?(x1), Rplus?(x1), Rnone?(x1), rcv(l,tg) declared in M, @i: A, R-base-ma(R), R-loc(R), k sends only on links in L, es realizer ind Rbframe compseq tag def, k affects only members of L, es realizer ind Raframe compseq tag def, (with ds: ds action a:T precondition a(v) is P s v), es realizer ind Rpre compseq tag def, with declarations ds:dsda:dak(v) sends f s v on link l, f  g, es realizer ind Rsends compseq tag def, with declarations ds:dsda:daeffect of k(v) is x := f s v, es realizer ind Reffect compseq tag def, only L sends on (l with tg), es realizer ind Rsframe compseq tag def, only members of L affect x :t, es realizer ind Rframe compseq tag def, x : t initially x = v, es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, @loc: only members of L read x, IdLnk, @loc: k sends only on links in L, @loc: k writes only members of L, @loc precondition for a(v:T):P State(ds) v, sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc effect knd(v:T) x := f State(ds) v , only events in L send on lnk with tag, @loc only events in L change x:T, @loc x initially v:T, left right,  , State(ds), DeclaredType(ds;x), rec(x.A(x)), Realizer |